(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const r4 Real)
(declare-const r6 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(declare-const r13 Real)
(declare-const r14 Real)
(declare-const r17 Real)
(declare-const r18 Real)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const r19 Real)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const r20 Real)
(declare-const v10 Bool)
(push)
(declare-const r21 Real)
(declare-const r22 Real)
(declare-const r23 Real)
(push)
(declare-const v11 Bool)
(declare-const r24 Real)
(assert (or (distinct 2154.0 9844.0 r18 r7) v4 (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2)))
(assert (or (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2) v10 (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2))))
(assert (or (< r6 r14 (/ 0.8545 r0)) v8 v3))
(assert (or (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2) (distinct 2154.0 9844.0 r18 r7) (distinct 2154.0 9844.0 r18 r7)))
(assert (or v2 v10 (distinct r17 r4 14.0 r17)))
(assert (or v3 v8 v4))
(assert (or v10 v4 (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2))))
(assert (or (not (> 80513625229.0 24.4797)) v10 (< r6 r14 (/ 0.8545 r0))))
(assert (or (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2)) (distinct r17 r4 14.0 r17) (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3)))))
(assert (or (< r6 r14 (/ 0.8545 r0)) v8 v4))
(assert (or (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2)) v3 (=> v7 (distinct r17 r4 14.0 r17))))
(assert (or v2 (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3))) v10))
(assert (or (=> v7 (distinct r17 r4 14.0 r17)) (< r6 r14 (/ 0.8545 r0)) (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2))))
(assert (or v8 v8 (< r6 r14 (/ 0.8545 r0))))
(assert (or v2 (distinct 2154.0 9844.0 r18 r7) v2))
(assert (or (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2)) v3 v10))
(assert (or v8 (=> v7 (distinct r17 r4 14.0 r17)) v3))
(assert (or v4 v4 (< r6 r14 (/ 0.8545 r0))))
(assert (or (distinct r17 r4 14.0 r17) v4 v8))
(assert (or (not (> 80513625229.0 24.4797)) v2 v3))
(assert (or v2 v4 (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3)))))
(assert (or (< r6 r14 (/ 0.8545 r0)) (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2)) (distinct r17 r4 14.0 r17)))
(assert (or (< r6 r14 (/ 0.8545 r0)) (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3))) v10))
(assert (or (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3))) (not (> 80513625229.0 24.4797)) (distinct 2154.0 9844.0 r18 r7)))
(assert (or (distinct r17 r4 14.0 r17) v8 (distinct r17 r4 14.0 r17)))
(assert (or v3 (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2) v4))
(assert (or (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2)) v2 (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3)))))
(assert (or (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3))) (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3))) (distinct r17 r4 14.0 r17)))
(assert (or (distinct r17 r4 14.0 r17) (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2)) v4))
(assert (or (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2) (not (> 80513625229.0 24.4797)) v2))
(assert (or (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2)) v3 (not (> 80513625229.0 24.4797))))
(assert (or (not (> 80513625229.0 24.4797)) (=> v7 (distinct r17 r4 14.0 r17)) v3))
(assert (or v4 (=> v7 (distinct r17 r4 14.0 r17)) v10))
(assert (or (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2) v2 v8))
(assert (or v2 (not (> 80513625229.0 24.4797)) (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2)))
(assert (or v8 (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3))) (not (> 80513625229.0 24.4797))))
(assert (or (distinct r17 r4 14.0 r17) (< r6 r14 (/ 0.8545 r0)) v2))
(assert (or (=> v7 (distinct r17 r4 14.0 r17)) (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3))) (=> v7 (distinct r17 r4 14.0 r17))))
(assert (or v2 v3 v2))
(assert (or v4 (not (> 80513625229.0 24.4797)) v8))
(assert (or v10 (distinct r17 r4 14.0 r17) (distinct 2154.0 9844.0 r18 r7)))
(assert (or (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3))) (not (> 80513625229.0 24.4797)) v4))
(assert (or (=> v7 (distinct r17 r4 14.0 r17)) v2 v4))
(assert (or v10 v2 v4))
(assert (or (distinct r17 r4 14.0 r17) (< r6 r21 (* (- (/ r17 r2)) 9844.0 r2)) v3))
(assert (or (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2) v10 (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2)))
(assert (or (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3))) (< r6 r14 (/ 0.8545 r0)) (or v5 v3 v6 v7 v10 v5 v0 (distinct 2154.0 9844.0 r18 r7) v6 (xor v9 v3 (xor (>= 14.0 r8 0.8545 80513625229.0) (<= 9844.0 9844.0) v4 v9 v3 v6 (> 80513625229.0 24.4797) v9 v3)))))
(assert (or (not (> 80513625229.0 24.4797)) (distinct 2154.0 9844.0 r18 r7) (< 80513625229.0 r13 800998.0 (* (- (/ r17 r2)) 9844.0 r2) r2)))
(assert (or (distinct 2154.0 9844.0 r18 r7) v2 v4))
(check-sat)
